0 Prolog
↳1 UnifyTransformerProof (⇔, 0 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 60 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 180 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇔, 11 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 PiDP
↳26 PiDPToQDPProof (⇒, 0 ms)
↳27 QDP
↳28 QDPSizeChangeProof (⇔, 0 ms)
↳29 YES
↳30 PiDP
↳31 PiDPToQDPProof (⇒, 0 ms)
↳32 QDP
↳33 Rewriting (⇔, 0 ms)
↳34 QDP
↳35 Rewriting (⇔, 4 ms)
↳36 QDP
↳37 Instantiation (⇔, 0 ms)
↳38 QDP
↳39 Rewriting (⇔, 0 ms)
↳40 QDP
↳41 Instantiation (⇔, 6 ms)
↳42 QDP
↳43 Rewriting (⇔, 0 ms)
↳44 QDP
↳45 QDPOrderProof (⇔, 206 ms)
↳46 QDP
↳47 DependencyGraphProof (⇔, 0 ms)
↳48 QDP
↳49 QDPOrderProof (⇔, 174 ms)
↳50 QDP
↳51 DependencyGraphProof (⇔, 0 ms)
↳52 TRUE
ways_in_gga(0, X1, s(0)) → ways_out_gga(0, X1, s(0))
ways_in_gga(X2, [], 0) → ways_out_gga(X2, [], 0)
ways_in_gga(Amount, .(s(C), Coins), N) → U4_gga(Amount, C, Coins, N, =_in_ga(Amount, s(X3)))
=_in_ga(X, X) → =_out_ga(X, X)
U4_gga(Amount, C, Coins, N, =_out_ga(Amount, s(X3))) → U5_gga(Amount, C, Coins, N, X3, plus_in_gag(s(C), NewAmount, Amount))
plus_in_gag(0, X, X) → U2_gag(X, nat_in_g(X))
nat_in_g(0) → nat_out_g(0)
nat_in_g(s(X)) → U1_g(X, nat_in_g(X))
U1_g(X, nat_out_g(X)) → nat_out_g(s(X))
U2_gag(X, nat_out_g(X)) → plus_out_gag(0, X, X)
plus_in_gag(s(X), Y, s(Z)) → U3_gag(X, Y, Z, plus_in_gag(X, Y, Z))
U3_gag(X, Y, Z, plus_out_gag(X, Y, Z)) → plus_out_gag(s(X), Y, s(Z))
U5_gga(Amount, C, Coins, N, X3, plus_out_gag(s(C), NewAmount, Amount)) → U6_gga(Amount, C, Coins, N, X3, NewAmount, ways_in_gga(Amount, Coins, N1))
ways_in_gga(Amount, .(s(C), Coins), N) → U9_gga(Amount, C, Coins, N, =_in_ga(Amount, s(X4)))
U9_gga(Amount, C, Coins, N, =_out_ga(Amount, s(X4))) → U10_gga(Amount, C, Coins, N, X4, plus_in_gag(Amount, s(X5), s(C)))
U10_gga(Amount, C, Coins, N, X4, plus_out_gag(Amount, s(X5), s(C))) → U11_gga(Amount, C, Coins, N, ways_in_gga(Amount, Coins, N))
U11_gga(Amount, C, Coins, N, ways_out_gga(Amount, Coins, N)) → ways_out_gga(Amount, .(s(C), Coins), N)
U6_gga(Amount, C, Coins, N, X3, NewAmount, ways_out_gga(Amount, Coins, N1)) → U7_gga(Amount, C, Coins, N, X3, NewAmount, N1, ways_in_gga(NewAmount, .(s(C), Coins), N2))
U7_gga(Amount, C, Coins, N, X3, NewAmount, N1, ways_out_gga(NewAmount, .(s(C), Coins), N2)) → U8_gga(Amount, C, Coins, N, plus_in_gga(N1, N2, N))
plus_in_gga(0, X, X) → U2_gga(X, nat_in_g(X))
U2_gga(X, nat_out_g(X)) → plus_out_gga(0, X, X)
plus_in_gga(s(X), Y, s(Z)) → U3_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U3_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U8_gga(Amount, C, Coins, N, plus_out_gga(N1, N2, N)) → ways_out_gga(Amount, .(s(C), Coins), N)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
ways_in_gga(0, X1, s(0)) → ways_out_gga(0, X1, s(0))
ways_in_gga(X2, [], 0) → ways_out_gga(X2, [], 0)
ways_in_gga(Amount, .(s(C), Coins), N) → U4_gga(Amount, C, Coins, N, =_in_ga(Amount, s(X3)))
=_in_ga(X, X) → =_out_ga(X, X)
U4_gga(Amount, C, Coins, N, =_out_ga(Amount, s(X3))) → U5_gga(Amount, C, Coins, N, X3, plus_in_gag(s(C), NewAmount, Amount))
plus_in_gag(0, X, X) → U2_gag(X, nat_in_g(X))
nat_in_g(0) → nat_out_g(0)
nat_in_g(s(X)) → U1_g(X, nat_in_g(X))
U1_g(X, nat_out_g(X)) → nat_out_g(s(X))
U2_gag(X, nat_out_g(X)) → plus_out_gag(0, X, X)
plus_in_gag(s(X), Y, s(Z)) → U3_gag(X, Y, Z, plus_in_gag(X, Y, Z))
U3_gag(X, Y, Z, plus_out_gag(X, Y, Z)) → plus_out_gag(s(X), Y, s(Z))
U5_gga(Amount, C, Coins, N, X3, plus_out_gag(s(C), NewAmount, Amount)) → U6_gga(Amount, C, Coins, N, X3, NewAmount, ways_in_gga(Amount, Coins, N1))
ways_in_gga(Amount, .(s(C), Coins), N) → U9_gga(Amount, C, Coins, N, =_in_ga(Amount, s(X4)))
U9_gga(Amount, C, Coins, N, =_out_ga(Amount, s(X4))) → U10_gga(Amount, C, Coins, N, X4, plus_in_gag(Amount, s(X5), s(C)))
U10_gga(Amount, C, Coins, N, X4, plus_out_gag(Amount, s(X5), s(C))) → U11_gga(Amount, C, Coins, N, ways_in_gga(Amount, Coins, N))
U11_gga(Amount, C, Coins, N, ways_out_gga(Amount, Coins, N)) → ways_out_gga(Amount, .(s(C), Coins), N)
U6_gga(Amount, C, Coins, N, X3, NewAmount, ways_out_gga(Amount, Coins, N1)) → U7_gga(Amount, C, Coins, N, X3, NewAmount, N1, ways_in_gga(NewAmount, .(s(C), Coins), N2))
U7_gga(Amount, C, Coins, N, X3, NewAmount, N1, ways_out_gga(NewAmount, .(s(C), Coins), N2)) → U8_gga(Amount, C, Coins, N, plus_in_gga(N1, N2, N))
plus_in_gga(0, X, X) → U2_gga(X, nat_in_g(X))
U2_gga(X, nat_out_g(X)) → plus_out_gga(0, X, X)
plus_in_gga(s(X), Y, s(Z)) → U3_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U3_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U8_gga(Amount, C, Coins, N, plus_out_gga(N1, N2, N)) → ways_out_gga(Amount, .(s(C), Coins), N)
WAYS_IN_GGA(Amount, .(s(C), Coins), N) → U4_GGA(Amount, C, Coins, N, =_in_ga(Amount, s(X3)))
WAYS_IN_GGA(Amount, .(s(C), Coins), N) → =_IN_GA(Amount, s(X3))
U4_GGA(Amount, C, Coins, N, =_out_ga(Amount, s(X3))) → U5_GGA(Amount, C, Coins, N, X3, plus_in_gag(s(C), NewAmount, Amount))
U4_GGA(Amount, C, Coins, N, =_out_ga(Amount, s(X3))) → PLUS_IN_GAG(s(C), NewAmount, Amount)
PLUS_IN_GAG(0, X, X) → U2_GAG(X, nat_in_g(X))
PLUS_IN_GAG(0, X, X) → NAT_IN_G(X)
NAT_IN_G(s(X)) → U1_G(X, nat_in_g(X))
NAT_IN_G(s(X)) → NAT_IN_G(X)
PLUS_IN_GAG(s(X), Y, s(Z)) → U3_GAG(X, Y, Z, plus_in_gag(X, Y, Z))
PLUS_IN_GAG(s(X), Y, s(Z)) → PLUS_IN_GAG(X, Y, Z)
U5_GGA(Amount, C, Coins, N, X3, plus_out_gag(s(C), NewAmount, Amount)) → U6_GGA(Amount, C, Coins, N, X3, NewAmount, ways_in_gga(Amount, Coins, N1))
U5_GGA(Amount, C, Coins, N, X3, plus_out_gag(s(C), NewAmount, Amount)) → WAYS_IN_GGA(Amount, Coins, N1)
WAYS_IN_GGA(Amount, .(s(C), Coins), N) → U9_GGA(Amount, C, Coins, N, =_in_ga(Amount, s(X4)))
U9_GGA(Amount, C, Coins, N, =_out_ga(Amount, s(X4))) → U10_GGA(Amount, C, Coins, N, X4, plus_in_gag(Amount, s(X5), s(C)))
U9_GGA(Amount, C, Coins, N, =_out_ga(Amount, s(X4))) → PLUS_IN_GAG(Amount, s(X5), s(C))
U10_GGA(Amount, C, Coins, N, X4, plus_out_gag(Amount, s(X5), s(C))) → U11_GGA(Amount, C, Coins, N, ways_in_gga(Amount, Coins, N))
U10_GGA(Amount, C, Coins, N, X4, plus_out_gag(Amount, s(X5), s(C))) → WAYS_IN_GGA(Amount, Coins, N)
U6_GGA(Amount, C, Coins, N, X3, NewAmount, ways_out_gga(Amount, Coins, N1)) → U7_GGA(Amount, C, Coins, N, X3, NewAmount, N1, ways_in_gga(NewAmount, .(s(C), Coins), N2))
U6_GGA(Amount, C, Coins, N, X3, NewAmount, ways_out_gga(Amount, Coins, N1)) → WAYS_IN_GGA(NewAmount, .(s(C), Coins), N2)
U7_GGA(Amount, C, Coins, N, X3, NewAmount, N1, ways_out_gga(NewAmount, .(s(C), Coins), N2)) → U8_GGA(Amount, C, Coins, N, plus_in_gga(N1, N2, N))
U7_GGA(Amount, C, Coins, N, X3, NewAmount, N1, ways_out_gga(NewAmount, .(s(C), Coins), N2)) → PLUS_IN_GGA(N1, N2, N)
PLUS_IN_GGA(0, X, X) → U2_GGA(X, nat_in_g(X))
PLUS_IN_GGA(0, X, X) → NAT_IN_G(X)
PLUS_IN_GGA(s(X), Y, s(Z)) → U3_GGA(X, Y, Z, plus_in_gga(X, Y, Z))
PLUS_IN_GGA(s(X), Y, s(Z)) → PLUS_IN_GGA(X, Y, Z)
ways_in_gga(0, X1, s(0)) → ways_out_gga(0, X1, s(0))
ways_in_gga(X2, [], 0) → ways_out_gga(X2, [], 0)
ways_in_gga(Amount, .(s(C), Coins), N) → U4_gga(Amount, C, Coins, N, =_in_ga(Amount, s(X3)))
=_in_ga(X, X) → =_out_ga(X, X)
U4_gga(Amount, C, Coins, N, =_out_ga(Amount, s(X3))) → U5_gga(Amount, C, Coins, N, X3, plus_in_gag(s(C), NewAmount, Amount))
plus_in_gag(0, X, X) → U2_gag(X, nat_in_g(X))
nat_in_g(0) → nat_out_g(0)
nat_in_g(s(X)) → U1_g(X, nat_in_g(X))
U1_g(X, nat_out_g(X)) → nat_out_g(s(X))
U2_gag(X, nat_out_g(X)) → plus_out_gag(0, X, X)
plus_in_gag(s(X), Y, s(Z)) → U3_gag(X, Y, Z, plus_in_gag(X, Y, Z))
U3_gag(X, Y, Z, plus_out_gag(X, Y, Z)) → plus_out_gag(s(X), Y, s(Z))
U5_gga(Amount, C, Coins, N, X3, plus_out_gag(s(C), NewAmount, Amount)) → U6_gga(Amount, C, Coins, N, X3, NewAmount, ways_in_gga(Amount, Coins, N1))
ways_in_gga(Amount, .(s(C), Coins), N) → U9_gga(Amount, C, Coins, N, =_in_ga(Amount, s(X4)))
U9_gga(Amount, C, Coins, N, =_out_ga(Amount, s(X4))) → U10_gga(Amount, C, Coins, N, X4, plus_in_gag(Amount, s(X5), s(C)))
U10_gga(Amount, C, Coins, N, X4, plus_out_gag(Amount, s(X5), s(C))) → U11_gga(Amount, C, Coins, N, ways_in_gga(Amount, Coins, N))
U11_gga(Amount, C, Coins, N, ways_out_gga(Amount, Coins, N)) → ways_out_gga(Amount, .(s(C), Coins), N)
U6_gga(Amount, C, Coins, N, X3, NewAmount, ways_out_gga(Amount, Coins, N1)) → U7_gga(Amount, C, Coins, N, X3, NewAmount, N1, ways_in_gga(NewAmount, .(s(C), Coins), N2))
U7_gga(Amount, C, Coins, N, X3, NewAmount, N1, ways_out_gga(NewAmount, .(s(C), Coins), N2)) → U8_gga(Amount, C, Coins, N, plus_in_gga(N1, N2, N))
plus_in_gga(0, X, X) → U2_gga(X, nat_in_g(X))
U2_gga(X, nat_out_g(X)) → plus_out_gga(0, X, X)
plus_in_gga(s(X), Y, s(Z)) → U3_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U3_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U8_gga(Amount, C, Coins, N, plus_out_gga(N1, N2, N)) → ways_out_gga(Amount, .(s(C), Coins), N)
WAYS_IN_GGA(Amount, .(s(C), Coins), N) → U4_GGA(Amount, C, Coins, N, =_in_ga(Amount, s(X3)))
WAYS_IN_GGA(Amount, .(s(C), Coins), N) → =_IN_GA(Amount, s(X3))
U4_GGA(Amount, C, Coins, N, =_out_ga(Amount, s(X3))) → U5_GGA(Amount, C, Coins, N, X3, plus_in_gag(s(C), NewAmount, Amount))
U4_GGA(Amount, C, Coins, N, =_out_ga(Amount, s(X3))) → PLUS_IN_GAG(s(C), NewAmount, Amount)
PLUS_IN_GAG(0, X, X) → U2_GAG(X, nat_in_g(X))
PLUS_IN_GAG(0, X, X) → NAT_IN_G(X)
NAT_IN_G(s(X)) → U1_G(X, nat_in_g(X))
NAT_IN_G(s(X)) → NAT_IN_G(X)
PLUS_IN_GAG(s(X), Y, s(Z)) → U3_GAG(X, Y, Z, plus_in_gag(X, Y, Z))
PLUS_IN_GAG(s(X), Y, s(Z)) → PLUS_IN_GAG(X, Y, Z)
U5_GGA(Amount, C, Coins, N, X3, plus_out_gag(s(C), NewAmount, Amount)) → U6_GGA(Amount, C, Coins, N, X3, NewAmount, ways_in_gga(Amount, Coins, N1))
U5_GGA(Amount, C, Coins, N, X3, plus_out_gag(s(C), NewAmount, Amount)) → WAYS_IN_GGA(Amount, Coins, N1)
WAYS_IN_GGA(Amount, .(s(C), Coins), N) → U9_GGA(Amount, C, Coins, N, =_in_ga(Amount, s(X4)))
U9_GGA(Amount, C, Coins, N, =_out_ga(Amount, s(X4))) → U10_GGA(Amount, C, Coins, N, X4, plus_in_gag(Amount, s(X5), s(C)))
U9_GGA(Amount, C, Coins, N, =_out_ga(Amount, s(X4))) → PLUS_IN_GAG(Amount, s(X5), s(C))
U10_GGA(Amount, C, Coins, N, X4, plus_out_gag(Amount, s(X5), s(C))) → U11_GGA(Amount, C, Coins, N, ways_in_gga(Amount, Coins, N))
U10_GGA(Amount, C, Coins, N, X4, plus_out_gag(Amount, s(X5), s(C))) → WAYS_IN_GGA(Amount, Coins, N)
U6_GGA(Amount, C, Coins, N, X3, NewAmount, ways_out_gga(Amount, Coins, N1)) → U7_GGA(Amount, C, Coins, N, X3, NewAmount, N1, ways_in_gga(NewAmount, .(s(C), Coins), N2))
U6_GGA(Amount, C, Coins, N, X3, NewAmount, ways_out_gga(Amount, Coins, N1)) → WAYS_IN_GGA(NewAmount, .(s(C), Coins), N2)
U7_GGA(Amount, C, Coins, N, X3, NewAmount, N1, ways_out_gga(NewAmount, .(s(C), Coins), N2)) → U8_GGA(Amount, C, Coins, N, plus_in_gga(N1, N2, N))
U7_GGA(Amount, C, Coins, N, X3, NewAmount, N1, ways_out_gga(NewAmount, .(s(C), Coins), N2)) → PLUS_IN_GGA(N1, N2, N)
PLUS_IN_GGA(0, X, X) → U2_GGA(X, nat_in_g(X))
PLUS_IN_GGA(0, X, X) → NAT_IN_G(X)
PLUS_IN_GGA(s(X), Y, s(Z)) → U3_GGA(X, Y, Z, plus_in_gga(X, Y, Z))
PLUS_IN_GGA(s(X), Y, s(Z)) → PLUS_IN_GGA(X, Y, Z)
ways_in_gga(0, X1, s(0)) → ways_out_gga(0, X1, s(0))
ways_in_gga(X2, [], 0) → ways_out_gga(X2, [], 0)
ways_in_gga(Amount, .(s(C), Coins), N) → U4_gga(Amount, C, Coins, N, =_in_ga(Amount, s(X3)))
=_in_ga(X, X) → =_out_ga(X, X)
U4_gga(Amount, C, Coins, N, =_out_ga(Amount, s(X3))) → U5_gga(Amount, C, Coins, N, X3, plus_in_gag(s(C), NewAmount, Amount))
plus_in_gag(0, X, X) → U2_gag(X, nat_in_g(X))
nat_in_g(0) → nat_out_g(0)
nat_in_g(s(X)) → U1_g(X, nat_in_g(X))
U1_g(X, nat_out_g(X)) → nat_out_g(s(X))
U2_gag(X, nat_out_g(X)) → plus_out_gag(0, X, X)
plus_in_gag(s(X), Y, s(Z)) → U3_gag(X, Y, Z, plus_in_gag(X, Y, Z))
U3_gag(X, Y, Z, plus_out_gag(X, Y, Z)) → plus_out_gag(s(X), Y, s(Z))
U5_gga(Amount, C, Coins, N, X3, plus_out_gag(s(C), NewAmount, Amount)) → U6_gga(Amount, C, Coins, N, X3, NewAmount, ways_in_gga(Amount, Coins, N1))
ways_in_gga(Amount, .(s(C), Coins), N) → U9_gga(Amount, C, Coins, N, =_in_ga(Amount, s(X4)))
U9_gga(Amount, C, Coins, N, =_out_ga(Amount, s(X4))) → U10_gga(Amount, C, Coins, N, X4, plus_in_gag(Amount, s(X5), s(C)))
U10_gga(Amount, C, Coins, N, X4, plus_out_gag(Amount, s(X5), s(C))) → U11_gga(Amount, C, Coins, N, ways_in_gga(Amount, Coins, N))
U11_gga(Amount, C, Coins, N, ways_out_gga(Amount, Coins, N)) → ways_out_gga(Amount, .(s(C), Coins), N)
U6_gga(Amount, C, Coins, N, X3, NewAmount, ways_out_gga(Amount, Coins, N1)) → U7_gga(Amount, C, Coins, N, X3, NewAmount, N1, ways_in_gga(NewAmount, .(s(C), Coins), N2))
U7_gga(Amount, C, Coins, N, X3, NewAmount, N1, ways_out_gga(NewAmount, .(s(C), Coins), N2)) → U8_gga(Amount, C, Coins, N, plus_in_gga(N1, N2, N))
plus_in_gga(0, X, X) → U2_gga(X, nat_in_g(X))
U2_gga(X, nat_out_g(X)) → plus_out_gga(0, X, X)
plus_in_gga(s(X), Y, s(Z)) → U3_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U3_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U8_gga(Amount, C, Coins, N, plus_out_gga(N1, N2, N)) → ways_out_gga(Amount, .(s(C), Coins), N)
NAT_IN_G(s(X)) → NAT_IN_G(X)
ways_in_gga(0, X1, s(0)) → ways_out_gga(0, X1, s(0))
ways_in_gga(X2, [], 0) → ways_out_gga(X2, [], 0)
ways_in_gga(Amount, .(s(C), Coins), N) → U4_gga(Amount, C, Coins, N, =_in_ga(Amount, s(X3)))
=_in_ga(X, X) → =_out_ga(X, X)
U4_gga(Amount, C, Coins, N, =_out_ga(Amount, s(X3))) → U5_gga(Amount, C, Coins, N, X3, plus_in_gag(s(C), NewAmount, Amount))
plus_in_gag(0, X, X) → U2_gag(X, nat_in_g(X))
nat_in_g(0) → nat_out_g(0)
nat_in_g(s(X)) → U1_g(X, nat_in_g(X))
U1_g(X, nat_out_g(X)) → nat_out_g(s(X))
U2_gag(X, nat_out_g(X)) → plus_out_gag(0, X, X)
plus_in_gag(s(X), Y, s(Z)) → U3_gag(X, Y, Z, plus_in_gag(X, Y, Z))
U3_gag(X, Y, Z, plus_out_gag(X, Y, Z)) → plus_out_gag(s(X), Y, s(Z))
U5_gga(Amount, C, Coins, N, X3, plus_out_gag(s(C), NewAmount, Amount)) → U6_gga(Amount, C, Coins, N, X3, NewAmount, ways_in_gga(Amount, Coins, N1))
ways_in_gga(Amount, .(s(C), Coins), N) → U9_gga(Amount, C, Coins, N, =_in_ga(Amount, s(X4)))
U9_gga(Amount, C, Coins, N, =_out_ga(Amount, s(X4))) → U10_gga(Amount, C, Coins, N, X4, plus_in_gag(Amount, s(X5), s(C)))
U10_gga(Amount, C, Coins, N, X4, plus_out_gag(Amount, s(X5), s(C))) → U11_gga(Amount, C, Coins, N, ways_in_gga(Amount, Coins, N))
U11_gga(Amount, C, Coins, N, ways_out_gga(Amount, Coins, N)) → ways_out_gga(Amount, .(s(C), Coins), N)
U6_gga(Amount, C, Coins, N, X3, NewAmount, ways_out_gga(Amount, Coins, N1)) → U7_gga(Amount, C, Coins, N, X3, NewAmount, N1, ways_in_gga(NewAmount, .(s(C), Coins), N2))
U7_gga(Amount, C, Coins, N, X3, NewAmount, N1, ways_out_gga(NewAmount, .(s(C), Coins), N2)) → U8_gga(Amount, C, Coins, N, plus_in_gga(N1, N2, N))
plus_in_gga(0, X, X) → U2_gga(X, nat_in_g(X))
U2_gga(X, nat_out_g(X)) → plus_out_gga(0, X, X)
plus_in_gga(s(X), Y, s(Z)) → U3_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U3_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U8_gga(Amount, C, Coins, N, plus_out_gga(N1, N2, N)) → ways_out_gga(Amount, .(s(C), Coins), N)
NAT_IN_G(s(X)) → NAT_IN_G(X)
NAT_IN_G(s(X)) → NAT_IN_G(X)
From the DPs we obtained the following set of size-change graphs:
PLUS_IN_GGA(s(X), Y, s(Z)) → PLUS_IN_GGA(X, Y, Z)
ways_in_gga(0, X1, s(0)) → ways_out_gga(0, X1, s(0))
ways_in_gga(X2, [], 0) → ways_out_gga(X2, [], 0)
ways_in_gga(Amount, .(s(C), Coins), N) → U4_gga(Amount, C, Coins, N, =_in_ga(Amount, s(X3)))
=_in_ga(X, X) → =_out_ga(X, X)
U4_gga(Amount, C, Coins, N, =_out_ga(Amount, s(X3))) → U5_gga(Amount, C, Coins, N, X3, plus_in_gag(s(C), NewAmount, Amount))
plus_in_gag(0, X, X) → U2_gag(X, nat_in_g(X))
nat_in_g(0) → nat_out_g(0)
nat_in_g(s(X)) → U1_g(X, nat_in_g(X))
U1_g(X, nat_out_g(X)) → nat_out_g(s(X))
U2_gag(X, nat_out_g(X)) → plus_out_gag(0, X, X)
plus_in_gag(s(X), Y, s(Z)) → U3_gag(X, Y, Z, plus_in_gag(X, Y, Z))
U3_gag(X, Y, Z, plus_out_gag(X, Y, Z)) → plus_out_gag(s(X), Y, s(Z))
U5_gga(Amount, C, Coins, N, X3, plus_out_gag(s(C), NewAmount, Amount)) → U6_gga(Amount, C, Coins, N, X3, NewAmount, ways_in_gga(Amount, Coins, N1))
ways_in_gga(Amount, .(s(C), Coins), N) → U9_gga(Amount, C, Coins, N, =_in_ga(Amount, s(X4)))
U9_gga(Amount, C, Coins, N, =_out_ga(Amount, s(X4))) → U10_gga(Amount, C, Coins, N, X4, plus_in_gag(Amount, s(X5), s(C)))
U10_gga(Amount, C, Coins, N, X4, plus_out_gag(Amount, s(X5), s(C))) → U11_gga(Amount, C, Coins, N, ways_in_gga(Amount, Coins, N))
U11_gga(Amount, C, Coins, N, ways_out_gga(Amount, Coins, N)) → ways_out_gga(Amount, .(s(C), Coins), N)
U6_gga(Amount, C, Coins, N, X3, NewAmount, ways_out_gga(Amount, Coins, N1)) → U7_gga(Amount, C, Coins, N, X3, NewAmount, N1, ways_in_gga(NewAmount, .(s(C), Coins), N2))
U7_gga(Amount, C, Coins, N, X3, NewAmount, N1, ways_out_gga(NewAmount, .(s(C), Coins), N2)) → U8_gga(Amount, C, Coins, N, plus_in_gga(N1, N2, N))
plus_in_gga(0, X, X) → U2_gga(X, nat_in_g(X))
U2_gga(X, nat_out_g(X)) → plus_out_gga(0, X, X)
plus_in_gga(s(X), Y, s(Z)) → U3_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U3_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U8_gga(Amount, C, Coins, N, plus_out_gga(N1, N2, N)) → ways_out_gga(Amount, .(s(C), Coins), N)
PLUS_IN_GGA(s(X), Y, s(Z)) → PLUS_IN_GGA(X, Y, Z)
PLUS_IN_GGA(s(X), Y) → PLUS_IN_GGA(X, Y)
From the DPs we obtained the following set of size-change graphs:
PLUS_IN_GAG(s(X), Y, s(Z)) → PLUS_IN_GAG(X, Y, Z)
ways_in_gga(0, X1, s(0)) → ways_out_gga(0, X1, s(0))
ways_in_gga(X2, [], 0) → ways_out_gga(X2, [], 0)
ways_in_gga(Amount, .(s(C), Coins), N) → U4_gga(Amount, C, Coins, N, =_in_ga(Amount, s(X3)))
=_in_ga(X, X) → =_out_ga(X, X)
U4_gga(Amount, C, Coins, N, =_out_ga(Amount, s(X3))) → U5_gga(Amount, C, Coins, N, X3, plus_in_gag(s(C), NewAmount, Amount))
plus_in_gag(0, X, X) → U2_gag(X, nat_in_g(X))
nat_in_g(0) → nat_out_g(0)
nat_in_g(s(X)) → U1_g(X, nat_in_g(X))
U1_g(X, nat_out_g(X)) → nat_out_g(s(X))
U2_gag(X, nat_out_g(X)) → plus_out_gag(0, X, X)
plus_in_gag(s(X), Y, s(Z)) → U3_gag(X, Y, Z, plus_in_gag(X, Y, Z))
U3_gag(X, Y, Z, plus_out_gag(X, Y, Z)) → plus_out_gag(s(X), Y, s(Z))
U5_gga(Amount, C, Coins, N, X3, plus_out_gag(s(C), NewAmount, Amount)) → U6_gga(Amount, C, Coins, N, X3, NewAmount, ways_in_gga(Amount, Coins, N1))
ways_in_gga(Amount, .(s(C), Coins), N) → U9_gga(Amount, C, Coins, N, =_in_ga(Amount, s(X4)))
U9_gga(Amount, C, Coins, N, =_out_ga(Amount, s(X4))) → U10_gga(Amount, C, Coins, N, X4, plus_in_gag(Amount, s(X5), s(C)))
U10_gga(Amount, C, Coins, N, X4, plus_out_gag(Amount, s(X5), s(C))) → U11_gga(Amount, C, Coins, N, ways_in_gga(Amount, Coins, N))
U11_gga(Amount, C, Coins, N, ways_out_gga(Amount, Coins, N)) → ways_out_gga(Amount, .(s(C), Coins), N)
U6_gga(Amount, C, Coins, N, X3, NewAmount, ways_out_gga(Amount, Coins, N1)) → U7_gga(Amount, C, Coins, N, X3, NewAmount, N1, ways_in_gga(NewAmount, .(s(C), Coins), N2))
U7_gga(Amount, C, Coins, N, X3, NewAmount, N1, ways_out_gga(NewAmount, .(s(C), Coins), N2)) → U8_gga(Amount, C, Coins, N, plus_in_gga(N1, N2, N))
plus_in_gga(0, X, X) → U2_gga(X, nat_in_g(X))
U2_gga(X, nat_out_g(X)) → plus_out_gga(0, X, X)
plus_in_gga(s(X), Y, s(Z)) → U3_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U3_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U8_gga(Amount, C, Coins, N, plus_out_gga(N1, N2, N)) → ways_out_gga(Amount, .(s(C), Coins), N)
PLUS_IN_GAG(s(X), Y, s(Z)) → PLUS_IN_GAG(X, Y, Z)
PLUS_IN_GAG(s(X), s(Z)) → PLUS_IN_GAG(X, Z)
From the DPs we obtained the following set of size-change graphs:
U4_GGA(Amount, C, Coins, N, =_out_ga(Amount, s(X3))) → U5_GGA(Amount, C, Coins, N, X3, plus_in_gag(s(C), NewAmount, Amount))
U5_GGA(Amount, C, Coins, N, X3, plus_out_gag(s(C), NewAmount, Amount)) → U6_GGA(Amount, C, Coins, N, X3, NewAmount, ways_in_gga(Amount, Coins, N1))
U6_GGA(Amount, C, Coins, N, X3, NewAmount, ways_out_gga(Amount, Coins, N1)) → WAYS_IN_GGA(NewAmount, .(s(C), Coins), N2)
WAYS_IN_GGA(Amount, .(s(C), Coins), N) → U4_GGA(Amount, C, Coins, N, =_in_ga(Amount, s(X3)))
WAYS_IN_GGA(Amount, .(s(C), Coins), N) → U9_GGA(Amount, C, Coins, N, =_in_ga(Amount, s(X4)))
U9_GGA(Amount, C, Coins, N, =_out_ga(Amount, s(X4))) → U10_GGA(Amount, C, Coins, N, X4, plus_in_gag(Amount, s(X5), s(C)))
U10_GGA(Amount, C, Coins, N, X4, plus_out_gag(Amount, s(X5), s(C))) → WAYS_IN_GGA(Amount, Coins, N)
U5_GGA(Amount, C, Coins, N, X3, plus_out_gag(s(C), NewAmount, Amount)) → WAYS_IN_GGA(Amount, Coins, N1)
ways_in_gga(0, X1, s(0)) → ways_out_gga(0, X1, s(0))
ways_in_gga(X2, [], 0) → ways_out_gga(X2, [], 0)
ways_in_gga(Amount, .(s(C), Coins), N) → U4_gga(Amount, C, Coins, N, =_in_ga(Amount, s(X3)))
=_in_ga(X, X) → =_out_ga(X, X)
U4_gga(Amount, C, Coins, N, =_out_ga(Amount, s(X3))) → U5_gga(Amount, C, Coins, N, X3, plus_in_gag(s(C), NewAmount, Amount))
plus_in_gag(0, X, X) → U2_gag(X, nat_in_g(X))
nat_in_g(0) → nat_out_g(0)
nat_in_g(s(X)) → U1_g(X, nat_in_g(X))
U1_g(X, nat_out_g(X)) → nat_out_g(s(X))
U2_gag(X, nat_out_g(X)) → plus_out_gag(0, X, X)
plus_in_gag(s(X), Y, s(Z)) → U3_gag(X, Y, Z, plus_in_gag(X, Y, Z))
U3_gag(X, Y, Z, plus_out_gag(X, Y, Z)) → plus_out_gag(s(X), Y, s(Z))
U5_gga(Amount, C, Coins, N, X3, plus_out_gag(s(C), NewAmount, Amount)) → U6_gga(Amount, C, Coins, N, X3, NewAmount, ways_in_gga(Amount, Coins, N1))
ways_in_gga(Amount, .(s(C), Coins), N) → U9_gga(Amount, C, Coins, N, =_in_ga(Amount, s(X4)))
U9_gga(Amount, C, Coins, N, =_out_ga(Amount, s(X4))) → U10_gga(Amount, C, Coins, N, X4, plus_in_gag(Amount, s(X5), s(C)))
U10_gga(Amount, C, Coins, N, X4, plus_out_gag(Amount, s(X5), s(C))) → U11_gga(Amount, C, Coins, N, ways_in_gga(Amount, Coins, N))
U11_gga(Amount, C, Coins, N, ways_out_gga(Amount, Coins, N)) → ways_out_gga(Amount, .(s(C), Coins), N)
U6_gga(Amount, C, Coins, N, X3, NewAmount, ways_out_gga(Amount, Coins, N1)) → U7_gga(Amount, C, Coins, N, X3, NewAmount, N1, ways_in_gga(NewAmount, .(s(C), Coins), N2))
U7_gga(Amount, C, Coins, N, X3, NewAmount, N1, ways_out_gga(NewAmount, .(s(C), Coins), N2)) → U8_gga(Amount, C, Coins, N, plus_in_gga(N1, N2, N))
plus_in_gga(0, X, X) → U2_gga(X, nat_in_g(X))
U2_gga(X, nat_out_g(X)) → plus_out_gga(0, X, X)
plus_in_gga(s(X), Y, s(Z)) → U3_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U3_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U8_gga(Amount, C, Coins, N, plus_out_gga(N1, N2, N)) → ways_out_gga(Amount, .(s(C), Coins), N)
U4_GGA(Amount, C, Coins, =_out_ga(s(X3))) → U5_GGA(Amount, C, Coins, plus_in_gag(s(C), Amount))
U5_GGA(Amount, C, Coins, plus_out_gag(NewAmount)) → U6_GGA(C, Coins, NewAmount, ways_in_gga(Amount, Coins))
U6_GGA(C, Coins, NewAmount, ways_out_gga(N1)) → WAYS_IN_GGA(NewAmount, .(s(C), Coins))
WAYS_IN_GGA(Amount, .(s(C), Coins)) → U4_GGA(Amount, C, Coins, =_in_ga(Amount))
WAYS_IN_GGA(Amount, .(s(C), Coins)) → U9_GGA(Amount, C, Coins, =_in_ga(Amount))
U9_GGA(Amount, C, Coins, =_out_ga(s(X4))) → U10_GGA(Amount, Coins, plus_in_gag(Amount, s(C)))
U10_GGA(Amount, Coins, plus_out_gag(s(X5))) → WAYS_IN_GGA(Amount, Coins)
U5_GGA(Amount, C, Coins, plus_out_gag(NewAmount)) → WAYS_IN_GGA(Amount, Coins)
ways_in_gga(0, X1) → ways_out_gga(s(0))
ways_in_gga(X2, []) → ways_out_gga(0)
ways_in_gga(Amount, .(s(C), Coins)) → U4_gga(Amount, C, Coins, =_in_ga(Amount))
=_in_ga(X) → =_out_ga(X)
U4_gga(Amount, C, Coins, =_out_ga(s(X3))) → U5_gga(Amount, C, Coins, plus_in_gag(s(C), Amount))
plus_in_gag(0, X) → U2_gag(X, nat_in_g(X))
nat_in_g(0) → nat_out_g
nat_in_g(s(X)) → U1_g(nat_in_g(X))
U1_g(nat_out_g) → nat_out_g
U2_gag(X, nat_out_g) → plus_out_gag(X)
plus_in_gag(s(X), s(Z)) → U3_gag(plus_in_gag(X, Z))
U3_gag(plus_out_gag(Y)) → plus_out_gag(Y)
U5_gga(Amount, C, Coins, plus_out_gag(NewAmount)) → U6_gga(C, Coins, NewAmount, ways_in_gga(Amount, Coins))
ways_in_gga(Amount, .(s(C), Coins)) → U9_gga(Amount, C, Coins, =_in_ga(Amount))
U9_gga(Amount, C, Coins, =_out_ga(s(X4))) → U10_gga(Amount, Coins, plus_in_gag(Amount, s(C)))
U10_gga(Amount, Coins, plus_out_gag(s(X5))) → U11_gga(ways_in_gga(Amount, Coins))
U11_gga(ways_out_gga(N)) → ways_out_gga(N)
U6_gga(C, Coins, NewAmount, ways_out_gga(N1)) → U7_gga(N1, ways_in_gga(NewAmount, .(s(C), Coins)))
U7_gga(N1, ways_out_gga(N2)) → U8_gga(plus_in_gga(N1, N2))
plus_in_gga(0, X) → U2_gga(X, nat_in_g(X))
U2_gga(X, nat_out_g) → plus_out_gga(X)
plus_in_gga(s(X), Y) → U3_gga(plus_in_gga(X, Y))
U3_gga(plus_out_gga(Z)) → plus_out_gga(s(Z))
U8_gga(plus_out_gga(N)) → ways_out_gga(N)
ways_in_gga(x0, x1)
=_in_ga(x0)
U4_gga(x0, x1, x2, x3)
plus_in_gag(x0, x1)
nat_in_g(x0)
U1_g(x0)
U2_gag(x0, x1)
U3_gag(x0)
U5_gga(x0, x1, x2, x3)
U9_gga(x0, x1, x2, x3)
U10_gga(x0, x1, x2)
U11_gga(x0)
U6_gga(x0, x1, x2, x3)
U7_gga(x0, x1)
plus_in_gga(x0, x1)
U2_gga(x0, x1)
U3_gga(x0)
U8_gga(x0)
WAYS_IN_GGA(Amount, .(s(C), Coins)) → U4_GGA(Amount, C, Coins, =_out_ga(Amount))
U4_GGA(Amount, C, Coins, =_out_ga(s(X3))) → U5_GGA(Amount, C, Coins, plus_in_gag(s(C), Amount))
U5_GGA(Amount, C, Coins, plus_out_gag(NewAmount)) → U6_GGA(C, Coins, NewAmount, ways_in_gga(Amount, Coins))
U6_GGA(C, Coins, NewAmount, ways_out_gga(N1)) → WAYS_IN_GGA(NewAmount, .(s(C), Coins))
WAYS_IN_GGA(Amount, .(s(C), Coins)) → U9_GGA(Amount, C, Coins, =_in_ga(Amount))
U9_GGA(Amount, C, Coins, =_out_ga(s(X4))) → U10_GGA(Amount, Coins, plus_in_gag(Amount, s(C)))
U10_GGA(Amount, Coins, plus_out_gag(s(X5))) → WAYS_IN_GGA(Amount, Coins)
U5_GGA(Amount, C, Coins, plus_out_gag(NewAmount)) → WAYS_IN_GGA(Amount, Coins)
WAYS_IN_GGA(Amount, .(s(C), Coins)) → U4_GGA(Amount, C, Coins, =_out_ga(Amount))
ways_in_gga(0, X1) → ways_out_gga(s(0))
ways_in_gga(X2, []) → ways_out_gga(0)
ways_in_gga(Amount, .(s(C), Coins)) → U4_gga(Amount, C, Coins, =_in_ga(Amount))
=_in_ga(X) → =_out_ga(X)
U4_gga(Amount, C, Coins, =_out_ga(s(X3))) → U5_gga(Amount, C, Coins, plus_in_gag(s(C), Amount))
plus_in_gag(0, X) → U2_gag(X, nat_in_g(X))
nat_in_g(0) → nat_out_g
nat_in_g(s(X)) → U1_g(nat_in_g(X))
U1_g(nat_out_g) → nat_out_g
U2_gag(X, nat_out_g) → plus_out_gag(X)
plus_in_gag(s(X), s(Z)) → U3_gag(plus_in_gag(X, Z))
U3_gag(plus_out_gag(Y)) → plus_out_gag(Y)
U5_gga(Amount, C, Coins, plus_out_gag(NewAmount)) → U6_gga(C, Coins, NewAmount, ways_in_gga(Amount, Coins))
ways_in_gga(Amount, .(s(C), Coins)) → U9_gga(Amount, C, Coins, =_in_ga(Amount))
U9_gga(Amount, C, Coins, =_out_ga(s(X4))) → U10_gga(Amount, Coins, plus_in_gag(Amount, s(C)))
U10_gga(Amount, Coins, plus_out_gag(s(X5))) → U11_gga(ways_in_gga(Amount, Coins))
U11_gga(ways_out_gga(N)) → ways_out_gga(N)
U6_gga(C, Coins, NewAmount, ways_out_gga(N1)) → U7_gga(N1, ways_in_gga(NewAmount, .(s(C), Coins)))
U7_gga(N1, ways_out_gga(N2)) → U8_gga(plus_in_gga(N1, N2))
plus_in_gga(0, X) → U2_gga(X, nat_in_g(X))
U2_gga(X, nat_out_g) → plus_out_gga(X)
plus_in_gga(s(X), Y) → U3_gga(plus_in_gga(X, Y))
U3_gga(plus_out_gga(Z)) → plus_out_gga(s(Z))
U8_gga(plus_out_gga(N)) → ways_out_gga(N)
ways_in_gga(x0, x1)
=_in_ga(x0)
U4_gga(x0, x1, x2, x3)
plus_in_gag(x0, x1)
nat_in_g(x0)
U1_g(x0)
U2_gag(x0, x1)
U3_gag(x0)
U5_gga(x0, x1, x2, x3)
U9_gga(x0, x1, x2, x3)
U10_gga(x0, x1, x2)
U11_gga(x0)
U6_gga(x0, x1, x2, x3)
U7_gga(x0, x1)
plus_in_gga(x0, x1)
U2_gga(x0, x1)
U3_gga(x0)
U8_gga(x0)
WAYS_IN_GGA(Amount, .(s(C), Coins)) → U9_GGA(Amount, C, Coins, =_out_ga(Amount))
U4_GGA(Amount, C, Coins, =_out_ga(s(X3))) → U5_GGA(Amount, C, Coins, plus_in_gag(s(C), Amount))
U5_GGA(Amount, C, Coins, plus_out_gag(NewAmount)) → U6_GGA(C, Coins, NewAmount, ways_in_gga(Amount, Coins))
U6_GGA(C, Coins, NewAmount, ways_out_gga(N1)) → WAYS_IN_GGA(NewAmount, .(s(C), Coins))
U9_GGA(Amount, C, Coins, =_out_ga(s(X4))) → U10_GGA(Amount, Coins, plus_in_gag(Amount, s(C)))
U10_GGA(Amount, Coins, plus_out_gag(s(X5))) → WAYS_IN_GGA(Amount, Coins)
U5_GGA(Amount, C, Coins, plus_out_gag(NewAmount)) → WAYS_IN_GGA(Amount, Coins)
WAYS_IN_GGA(Amount, .(s(C), Coins)) → U4_GGA(Amount, C, Coins, =_out_ga(Amount))
WAYS_IN_GGA(Amount, .(s(C), Coins)) → U9_GGA(Amount, C, Coins, =_out_ga(Amount))
ways_in_gga(0, X1) → ways_out_gga(s(0))
ways_in_gga(X2, []) → ways_out_gga(0)
ways_in_gga(Amount, .(s(C), Coins)) → U4_gga(Amount, C, Coins, =_in_ga(Amount))
=_in_ga(X) → =_out_ga(X)
U4_gga(Amount, C, Coins, =_out_ga(s(X3))) → U5_gga(Amount, C, Coins, plus_in_gag(s(C), Amount))
plus_in_gag(0, X) → U2_gag(X, nat_in_g(X))
nat_in_g(0) → nat_out_g
nat_in_g(s(X)) → U1_g(nat_in_g(X))
U1_g(nat_out_g) → nat_out_g
U2_gag(X, nat_out_g) → plus_out_gag(X)
plus_in_gag(s(X), s(Z)) → U3_gag(plus_in_gag(X, Z))
U3_gag(plus_out_gag(Y)) → plus_out_gag(Y)
U5_gga(Amount, C, Coins, plus_out_gag(NewAmount)) → U6_gga(C, Coins, NewAmount, ways_in_gga(Amount, Coins))
ways_in_gga(Amount, .(s(C), Coins)) → U9_gga(Amount, C, Coins, =_in_ga(Amount))
U9_gga(Amount, C, Coins, =_out_ga(s(X4))) → U10_gga(Amount, Coins, plus_in_gag(Amount, s(C)))
U10_gga(Amount, Coins, plus_out_gag(s(X5))) → U11_gga(ways_in_gga(Amount, Coins))
U11_gga(ways_out_gga(N)) → ways_out_gga(N)
U6_gga(C, Coins, NewAmount, ways_out_gga(N1)) → U7_gga(N1, ways_in_gga(NewAmount, .(s(C), Coins)))
U7_gga(N1, ways_out_gga(N2)) → U8_gga(plus_in_gga(N1, N2))
plus_in_gga(0, X) → U2_gga(X, nat_in_g(X))
U2_gga(X, nat_out_g) → plus_out_gga(X)
plus_in_gga(s(X), Y) → U3_gga(plus_in_gga(X, Y))
U3_gga(plus_out_gga(Z)) → plus_out_gga(s(Z))
U8_gga(plus_out_gga(N)) → ways_out_gga(N)
ways_in_gga(x0, x1)
=_in_ga(x0)
U4_gga(x0, x1, x2, x3)
plus_in_gag(x0, x1)
nat_in_g(x0)
U1_g(x0)
U2_gag(x0, x1)
U3_gag(x0)
U5_gga(x0, x1, x2, x3)
U9_gga(x0, x1, x2, x3)
U10_gga(x0, x1, x2)
U11_gga(x0)
U6_gga(x0, x1, x2, x3)
U7_gga(x0, x1)
plus_in_gga(x0, x1)
U2_gga(x0, x1)
U3_gga(x0)
U8_gga(x0)
U4_GGA(s(x3), z1, z2, =_out_ga(s(x3))) → U5_GGA(s(x3), z1, z2, plus_in_gag(s(z1), s(x3)))
U5_GGA(Amount, C, Coins, plus_out_gag(NewAmount)) → U6_GGA(C, Coins, NewAmount, ways_in_gga(Amount, Coins))
U6_GGA(C, Coins, NewAmount, ways_out_gga(N1)) → WAYS_IN_GGA(NewAmount, .(s(C), Coins))
U9_GGA(Amount, C, Coins, =_out_ga(s(X4))) → U10_GGA(Amount, Coins, plus_in_gag(Amount, s(C)))
U10_GGA(Amount, Coins, plus_out_gag(s(X5))) → WAYS_IN_GGA(Amount, Coins)
U5_GGA(Amount, C, Coins, plus_out_gag(NewAmount)) → WAYS_IN_GGA(Amount, Coins)
WAYS_IN_GGA(Amount, .(s(C), Coins)) → U4_GGA(Amount, C, Coins, =_out_ga(Amount))
WAYS_IN_GGA(Amount, .(s(C), Coins)) → U9_GGA(Amount, C, Coins, =_out_ga(Amount))
U4_GGA(s(x3), z1, z2, =_out_ga(s(x3))) → U5_GGA(s(x3), z1, z2, plus_in_gag(s(z1), s(x3)))
ways_in_gga(0, X1) → ways_out_gga(s(0))
ways_in_gga(X2, []) → ways_out_gga(0)
ways_in_gga(Amount, .(s(C), Coins)) → U4_gga(Amount, C, Coins, =_in_ga(Amount))
=_in_ga(X) → =_out_ga(X)
U4_gga(Amount, C, Coins, =_out_ga(s(X3))) → U5_gga(Amount, C, Coins, plus_in_gag(s(C), Amount))
plus_in_gag(0, X) → U2_gag(X, nat_in_g(X))
nat_in_g(0) → nat_out_g
nat_in_g(s(X)) → U1_g(nat_in_g(X))
U1_g(nat_out_g) → nat_out_g
U2_gag(X, nat_out_g) → plus_out_gag(X)
plus_in_gag(s(X), s(Z)) → U3_gag(plus_in_gag(X, Z))
U3_gag(plus_out_gag(Y)) → plus_out_gag(Y)
U5_gga(Amount, C, Coins, plus_out_gag(NewAmount)) → U6_gga(C, Coins, NewAmount, ways_in_gga(Amount, Coins))
ways_in_gga(Amount, .(s(C), Coins)) → U9_gga(Amount, C, Coins, =_in_ga(Amount))
U9_gga(Amount, C, Coins, =_out_ga(s(X4))) → U10_gga(Amount, Coins, plus_in_gag(Amount, s(C)))
U10_gga(Amount, Coins, plus_out_gag(s(X5))) → U11_gga(ways_in_gga(Amount, Coins))
U11_gga(ways_out_gga(N)) → ways_out_gga(N)
U6_gga(C, Coins, NewAmount, ways_out_gga(N1)) → U7_gga(N1, ways_in_gga(NewAmount, .(s(C), Coins)))
U7_gga(N1, ways_out_gga(N2)) → U8_gga(plus_in_gga(N1, N2))
plus_in_gga(0, X) → U2_gga(X, nat_in_g(X))
U2_gga(X, nat_out_g) → plus_out_gga(X)
plus_in_gga(s(X), Y) → U3_gga(plus_in_gga(X, Y))
U3_gga(plus_out_gga(Z)) → plus_out_gga(s(Z))
U8_gga(plus_out_gga(N)) → ways_out_gga(N)
ways_in_gga(x0, x1)
=_in_ga(x0)
U4_gga(x0, x1, x2, x3)
plus_in_gag(x0, x1)
nat_in_g(x0)
U1_g(x0)
U2_gag(x0, x1)
U3_gag(x0)
U5_gga(x0, x1, x2, x3)
U9_gga(x0, x1, x2, x3)
U10_gga(x0, x1, x2)
U11_gga(x0)
U6_gga(x0, x1, x2, x3)
U7_gga(x0, x1)
plus_in_gga(x0, x1)
U2_gga(x0, x1)
U3_gga(x0)
U8_gga(x0)
U4_GGA(s(x3), z1, z2, =_out_ga(s(x3))) → U5_GGA(s(x3), z1, z2, U3_gag(plus_in_gag(z1, x3)))
U5_GGA(Amount, C, Coins, plus_out_gag(NewAmount)) → U6_GGA(C, Coins, NewAmount, ways_in_gga(Amount, Coins))
U6_GGA(C, Coins, NewAmount, ways_out_gga(N1)) → WAYS_IN_GGA(NewAmount, .(s(C), Coins))
U9_GGA(Amount, C, Coins, =_out_ga(s(X4))) → U10_GGA(Amount, Coins, plus_in_gag(Amount, s(C)))
U10_GGA(Amount, Coins, plus_out_gag(s(X5))) → WAYS_IN_GGA(Amount, Coins)
U5_GGA(Amount, C, Coins, plus_out_gag(NewAmount)) → WAYS_IN_GGA(Amount, Coins)
WAYS_IN_GGA(Amount, .(s(C), Coins)) → U4_GGA(Amount, C, Coins, =_out_ga(Amount))
WAYS_IN_GGA(Amount, .(s(C), Coins)) → U9_GGA(Amount, C, Coins, =_out_ga(Amount))
U4_GGA(s(x3), z1, z2, =_out_ga(s(x3))) → U5_GGA(s(x3), z1, z2, U3_gag(plus_in_gag(z1, x3)))
ways_in_gga(0, X1) → ways_out_gga(s(0))
ways_in_gga(X2, []) → ways_out_gga(0)
ways_in_gga(Amount, .(s(C), Coins)) → U4_gga(Amount, C, Coins, =_in_ga(Amount))
=_in_ga(X) → =_out_ga(X)
U4_gga(Amount, C, Coins, =_out_ga(s(X3))) → U5_gga(Amount, C, Coins, plus_in_gag(s(C), Amount))
plus_in_gag(0, X) → U2_gag(X, nat_in_g(X))
nat_in_g(0) → nat_out_g
nat_in_g(s(X)) → U1_g(nat_in_g(X))
U1_g(nat_out_g) → nat_out_g
U2_gag(X, nat_out_g) → plus_out_gag(X)
plus_in_gag(s(X), s(Z)) → U3_gag(plus_in_gag(X, Z))
U3_gag(plus_out_gag(Y)) → plus_out_gag(Y)
U5_gga(Amount, C, Coins, plus_out_gag(NewAmount)) → U6_gga(C, Coins, NewAmount, ways_in_gga(Amount, Coins))
ways_in_gga(Amount, .(s(C), Coins)) → U9_gga(Amount, C, Coins, =_in_ga(Amount))
U9_gga(Amount, C, Coins, =_out_ga(s(X4))) → U10_gga(Amount, Coins, plus_in_gag(Amount, s(C)))
U10_gga(Amount, Coins, plus_out_gag(s(X5))) → U11_gga(ways_in_gga(Amount, Coins))
U11_gga(ways_out_gga(N)) → ways_out_gga(N)
U6_gga(C, Coins, NewAmount, ways_out_gga(N1)) → U7_gga(N1, ways_in_gga(NewAmount, .(s(C), Coins)))
U7_gga(N1, ways_out_gga(N2)) → U8_gga(plus_in_gga(N1, N2))
plus_in_gga(0, X) → U2_gga(X, nat_in_g(X))
U2_gga(X, nat_out_g) → plus_out_gga(X)
plus_in_gga(s(X), Y) → U3_gga(plus_in_gga(X, Y))
U3_gga(plus_out_gga(Z)) → plus_out_gga(s(Z))
U8_gga(plus_out_gga(N)) → ways_out_gga(N)
ways_in_gga(x0, x1)
=_in_ga(x0)
U4_gga(x0, x1, x2, x3)
plus_in_gag(x0, x1)
nat_in_g(x0)
U1_g(x0)
U2_gag(x0, x1)
U3_gag(x0)
U5_gga(x0, x1, x2, x3)
U9_gga(x0, x1, x2, x3)
U10_gga(x0, x1, x2)
U11_gga(x0)
U6_gga(x0, x1, x2, x3)
U7_gga(x0, x1)
plus_in_gga(x0, x1)
U2_gga(x0, x1)
U3_gga(x0)
U8_gga(x0)
U9_GGA(s(x3), z1, z2, =_out_ga(s(x3))) → U10_GGA(s(x3), z2, plus_in_gag(s(x3), s(z1)))
U5_GGA(Amount, C, Coins, plus_out_gag(NewAmount)) → U6_GGA(C, Coins, NewAmount, ways_in_gga(Amount, Coins))
U6_GGA(C, Coins, NewAmount, ways_out_gga(N1)) → WAYS_IN_GGA(NewAmount, .(s(C), Coins))
U10_GGA(Amount, Coins, plus_out_gag(s(X5))) → WAYS_IN_GGA(Amount, Coins)
U5_GGA(Amount, C, Coins, plus_out_gag(NewAmount)) → WAYS_IN_GGA(Amount, Coins)
WAYS_IN_GGA(Amount, .(s(C), Coins)) → U4_GGA(Amount, C, Coins, =_out_ga(Amount))
WAYS_IN_GGA(Amount, .(s(C), Coins)) → U9_GGA(Amount, C, Coins, =_out_ga(Amount))
U4_GGA(s(x3), z1, z2, =_out_ga(s(x3))) → U5_GGA(s(x3), z1, z2, U3_gag(plus_in_gag(z1, x3)))
U9_GGA(s(x3), z1, z2, =_out_ga(s(x3))) → U10_GGA(s(x3), z2, plus_in_gag(s(x3), s(z1)))
ways_in_gga(0, X1) → ways_out_gga(s(0))
ways_in_gga(X2, []) → ways_out_gga(0)
ways_in_gga(Amount, .(s(C), Coins)) → U4_gga(Amount, C, Coins, =_in_ga(Amount))
=_in_ga(X) → =_out_ga(X)
U4_gga(Amount, C, Coins, =_out_ga(s(X3))) → U5_gga(Amount, C, Coins, plus_in_gag(s(C), Amount))
plus_in_gag(0, X) → U2_gag(X, nat_in_g(X))
nat_in_g(0) → nat_out_g
nat_in_g(s(X)) → U1_g(nat_in_g(X))
U1_g(nat_out_g) → nat_out_g
U2_gag(X, nat_out_g) → plus_out_gag(X)
plus_in_gag(s(X), s(Z)) → U3_gag(plus_in_gag(X, Z))
U3_gag(plus_out_gag(Y)) → plus_out_gag(Y)
U5_gga(Amount, C, Coins, plus_out_gag(NewAmount)) → U6_gga(C, Coins, NewAmount, ways_in_gga(Amount, Coins))
ways_in_gga(Amount, .(s(C), Coins)) → U9_gga(Amount, C, Coins, =_in_ga(Amount))
U9_gga(Amount, C, Coins, =_out_ga(s(X4))) → U10_gga(Amount, Coins, plus_in_gag(Amount, s(C)))
U10_gga(Amount, Coins, plus_out_gag(s(X5))) → U11_gga(ways_in_gga(Amount, Coins))
U11_gga(ways_out_gga(N)) → ways_out_gga(N)
U6_gga(C, Coins, NewAmount, ways_out_gga(N1)) → U7_gga(N1, ways_in_gga(NewAmount, .(s(C), Coins)))
U7_gga(N1, ways_out_gga(N2)) → U8_gga(plus_in_gga(N1, N2))
plus_in_gga(0, X) → U2_gga(X, nat_in_g(X))
U2_gga(X, nat_out_g) → plus_out_gga(X)
plus_in_gga(s(X), Y) → U3_gga(plus_in_gga(X, Y))
U3_gga(plus_out_gga(Z)) → plus_out_gga(s(Z))
U8_gga(plus_out_gga(N)) → ways_out_gga(N)
ways_in_gga(x0, x1)
=_in_ga(x0)
U4_gga(x0, x1, x2, x3)
plus_in_gag(x0, x1)
nat_in_g(x0)
U1_g(x0)
U2_gag(x0, x1)
U3_gag(x0)
U5_gga(x0, x1, x2, x3)
U9_gga(x0, x1, x2, x3)
U10_gga(x0, x1, x2)
U11_gga(x0)
U6_gga(x0, x1, x2, x3)
U7_gga(x0, x1)
plus_in_gga(x0, x1)
U2_gga(x0, x1)
U3_gga(x0)
U8_gga(x0)
U9_GGA(s(x3), z1, z2, =_out_ga(s(x3))) → U10_GGA(s(x3), z2, U3_gag(plus_in_gag(x3, z1)))
U5_GGA(Amount, C, Coins, plus_out_gag(NewAmount)) → U6_GGA(C, Coins, NewAmount, ways_in_gga(Amount, Coins))
U6_GGA(C, Coins, NewAmount, ways_out_gga(N1)) → WAYS_IN_GGA(NewAmount, .(s(C), Coins))
U10_GGA(Amount, Coins, plus_out_gag(s(X5))) → WAYS_IN_GGA(Amount, Coins)
U5_GGA(Amount, C, Coins, plus_out_gag(NewAmount)) → WAYS_IN_GGA(Amount, Coins)
WAYS_IN_GGA(Amount, .(s(C), Coins)) → U4_GGA(Amount, C, Coins, =_out_ga(Amount))
WAYS_IN_GGA(Amount, .(s(C), Coins)) → U9_GGA(Amount, C, Coins, =_out_ga(Amount))
U4_GGA(s(x3), z1, z2, =_out_ga(s(x3))) → U5_GGA(s(x3), z1, z2, U3_gag(plus_in_gag(z1, x3)))
U9_GGA(s(x3), z1, z2, =_out_ga(s(x3))) → U10_GGA(s(x3), z2, U3_gag(plus_in_gag(x3, z1)))
ways_in_gga(0, X1) → ways_out_gga(s(0))
ways_in_gga(X2, []) → ways_out_gga(0)
ways_in_gga(Amount, .(s(C), Coins)) → U4_gga(Amount, C, Coins, =_in_ga(Amount))
=_in_ga(X) → =_out_ga(X)
U4_gga(Amount, C, Coins, =_out_ga(s(X3))) → U5_gga(Amount, C, Coins, plus_in_gag(s(C), Amount))
plus_in_gag(0, X) → U2_gag(X, nat_in_g(X))
nat_in_g(0) → nat_out_g
nat_in_g(s(X)) → U1_g(nat_in_g(X))
U1_g(nat_out_g) → nat_out_g
U2_gag(X, nat_out_g) → plus_out_gag(X)
plus_in_gag(s(X), s(Z)) → U3_gag(plus_in_gag(X, Z))
U3_gag(plus_out_gag(Y)) → plus_out_gag(Y)
U5_gga(Amount, C, Coins, plus_out_gag(NewAmount)) → U6_gga(C, Coins, NewAmount, ways_in_gga(Amount, Coins))
ways_in_gga(Amount, .(s(C), Coins)) → U9_gga(Amount, C, Coins, =_in_ga(Amount))
U9_gga(Amount, C, Coins, =_out_ga(s(X4))) → U10_gga(Amount, Coins, plus_in_gag(Amount, s(C)))
U10_gga(Amount, Coins, plus_out_gag(s(X5))) → U11_gga(ways_in_gga(Amount, Coins))
U11_gga(ways_out_gga(N)) → ways_out_gga(N)
U6_gga(C, Coins, NewAmount, ways_out_gga(N1)) → U7_gga(N1, ways_in_gga(NewAmount, .(s(C), Coins)))
U7_gga(N1, ways_out_gga(N2)) → U8_gga(plus_in_gga(N1, N2))
plus_in_gga(0, X) → U2_gga(X, nat_in_g(X))
U2_gga(X, nat_out_g) → plus_out_gga(X)
plus_in_gga(s(X), Y) → U3_gga(plus_in_gga(X, Y))
U3_gga(plus_out_gga(Z)) → plus_out_gga(s(Z))
U8_gga(plus_out_gga(N)) → ways_out_gga(N)
ways_in_gga(x0, x1)
=_in_ga(x0)
U4_gga(x0, x1, x2, x3)
plus_in_gag(x0, x1)
nat_in_g(x0)
U1_g(x0)
U2_gag(x0, x1)
U3_gag(x0)
U5_gga(x0, x1, x2, x3)
U9_gga(x0, x1, x2, x3)
U10_gga(x0, x1, x2)
U11_gga(x0)
U6_gga(x0, x1, x2, x3)
U7_gga(x0, x1)
plus_in_gga(x0, x1)
U2_gga(x0, x1)
U3_gga(x0)
U8_gga(x0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
U5_GGA(Amount, C, Coins, plus_out_gag(NewAmount)) → WAYS_IN_GGA(Amount, Coins)
WAYS_IN_GGA(Amount, .(s(C), Coins)) → U9_GGA(Amount, C, Coins, =_out_ga(Amount))
POL(.(x1, x2)) = 1 + x2
POL(0) = 0
POL(=_in_ga(x1)) = 1 + x1
POL(=_out_ga(x1)) = 0
POL(U10_GGA(x1, x2, x3)) = x2
POL(U10_gga(x1, x2, x3)) = 0
POL(U11_gga(x1)) = 0
POL(U1_g(x1)) = 0
POL(U2_gag(x1, x2)) = 0
POL(U2_gga(x1, x2)) = 0
POL(U3_gag(x1)) = 0
POL(U3_gga(x1)) = 0
POL(U4_GGA(x1, x2, x3, x4)) = 1 + x3
POL(U4_gga(x1, x2, x3, x4)) = 0
POL(U5_GGA(x1, x2, x3, x4)) = 1 + x3
POL(U5_gga(x1, x2, x3, x4)) = 0
POL(U6_GGA(x1, x2, x3, x4)) = 1 + x2
POL(U6_gga(x1, x2, x3, x4)) = 0
POL(U7_gga(x1, x2)) = 0
POL(U8_gga(x1)) = 0
POL(U9_GGA(x1, x2, x3, x4)) = x3
POL(U9_gga(x1, x2, x3, x4)) = 0
POL(WAYS_IN_GGA(x1, x2)) = x2
POL([]) = 0
POL(nat_in_g(x1)) = 1
POL(nat_out_g) = 0
POL(plus_in_gag(x1, x2)) = 0
POL(plus_in_gga(x1, x2)) = 1 + x2
POL(plus_out_gag(x1)) = 0
POL(plus_out_gga(x1)) = 0
POL(s(x1)) = 0
POL(ways_in_gga(x1, x2)) = 0
POL(ways_out_gga(x1)) = 0
U5_GGA(Amount, C, Coins, plus_out_gag(NewAmount)) → U6_GGA(C, Coins, NewAmount, ways_in_gga(Amount, Coins))
U6_GGA(C, Coins, NewAmount, ways_out_gga(N1)) → WAYS_IN_GGA(NewAmount, .(s(C), Coins))
U10_GGA(Amount, Coins, plus_out_gag(s(X5))) → WAYS_IN_GGA(Amount, Coins)
WAYS_IN_GGA(Amount, .(s(C), Coins)) → U4_GGA(Amount, C, Coins, =_out_ga(Amount))
U4_GGA(s(x3), z1, z2, =_out_ga(s(x3))) → U5_GGA(s(x3), z1, z2, U3_gag(plus_in_gag(z1, x3)))
U9_GGA(s(x3), z1, z2, =_out_ga(s(x3))) → U10_GGA(s(x3), z2, U3_gag(plus_in_gag(x3, z1)))
ways_in_gga(0, X1) → ways_out_gga(s(0))
ways_in_gga(X2, []) → ways_out_gga(0)
ways_in_gga(Amount, .(s(C), Coins)) → U4_gga(Amount, C, Coins, =_in_ga(Amount))
=_in_ga(X) → =_out_ga(X)
U4_gga(Amount, C, Coins, =_out_ga(s(X3))) → U5_gga(Amount, C, Coins, plus_in_gag(s(C), Amount))
plus_in_gag(0, X) → U2_gag(X, nat_in_g(X))
nat_in_g(0) → nat_out_g
nat_in_g(s(X)) → U1_g(nat_in_g(X))
U1_g(nat_out_g) → nat_out_g
U2_gag(X, nat_out_g) → plus_out_gag(X)
plus_in_gag(s(X), s(Z)) → U3_gag(plus_in_gag(X, Z))
U3_gag(plus_out_gag(Y)) → plus_out_gag(Y)
U5_gga(Amount, C, Coins, plus_out_gag(NewAmount)) → U6_gga(C, Coins, NewAmount, ways_in_gga(Amount, Coins))
ways_in_gga(Amount, .(s(C), Coins)) → U9_gga(Amount, C, Coins, =_in_ga(Amount))
U9_gga(Amount, C, Coins, =_out_ga(s(X4))) → U10_gga(Amount, Coins, plus_in_gag(Amount, s(C)))
U10_gga(Amount, Coins, plus_out_gag(s(X5))) → U11_gga(ways_in_gga(Amount, Coins))
U11_gga(ways_out_gga(N)) → ways_out_gga(N)
U6_gga(C, Coins, NewAmount, ways_out_gga(N1)) → U7_gga(N1, ways_in_gga(NewAmount, .(s(C), Coins)))
U7_gga(N1, ways_out_gga(N2)) → U8_gga(plus_in_gga(N1, N2))
plus_in_gga(0, X) → U2_gga(X, nat_in_g(X))
U2_gga(X, nat_out_g) → plus_out_gga(X)
plus_in_gga(s(X), Y) → U3_gga(plus_in_gga(X, Y))
U3_gga(plus_out_gga(Z)) → plus_out_gga(s(Z))
U8_gga(plus_out_gga(N)) → ways_out_gga(N)
ways_in_gga(x0, x1)
=_in_ga(x0)
U4_gga(x0, x1, x2, x3)
plus_in_gag(x0, x1)
nat_in_g(x0)
U1_g(x0)
U2_gag(x0, x1)
U3_gag(x0)
U5_gga(x0, x1, x2, x3)
U9_gga(x0, x1, x2, x3)
U10_gga(x0, x1, x2)
U11_gga(x0)
U6_gga(x0, x1, x2, x3)
U7_gga(x0, x1)
plus_in_gga(x0, x1)
U2_gga(x0, x1)
U3_gga(x0)
U8_gga(x0)
U6_GGA(C, Coins, NewAmount, ways_out_gga(N1)) → WAYS_IN_GGA(NewAmount, .(s(C), Coins))
WAYS_IN_GGA(Amount, .(s(C), Coins)) → U4_GGA(Amount, C, Coins, =_out_ga(Amount))
U4_GGA(s(x3), z1, z2, =_out_ga(s(x3))) → U5_GGA(s(x3), z1, z2, U3_gag(plus_in_gag(z1, x3)))
U5_GGA(Amount, C, Coins, plus_out_gag(NewAmount)) → U6_GGA(C, Coins, NewAmount, ways_in_gga(Amount, Coins))
ways_in_gga(0, X1) → ways_out_gga(s(0))
ways_in_gga(X2, []) → ways_out_gga(0)
ways_in_gga(Amount, .(s(C), Coins)) → U4_gga(Amount, C, Coins, =_in_ga(Amount))
=_in_ga(X) → =_out_ga(X)
U4_gga(Amount, C, Coins, =_out_ga(s(X3))) → U5_gga(Amount, C, Coins, plus_in_gag(s(C), Amount))
plus_in_gag(0, X) → U2_gag(X, nat_in_g(X))
nat_in_g(0) → nat_out_g
nat_in_g(s(X)) → U1_g(nat_in_g(X))
U1_g(nat_out_g) → nat_out_g
U2_gag(X, nat_out_g) → plus_out_gag(X)
plus_in_gag(s(X), s(Z)) → U3_gag(plus_in_gag(X, Z))
U3_gag(plus_out_gag(Y)) → plus_out_gag(Y)
U5_gga(Amount, C, Coins, plus_out_gag(NewAmount)) → U6_gga(C, Coins, NewAmount, ways_in_gga(Amount, Coins))
ways_in_gga(Amount, .(s(C), Coins)) → U9_gga(Amount, C, Coins, =_in_ga(Amount))
U9_gga(Amount, C, Coins, =_out_ga(s(X4))) → U10_gga(Amount, Coins, plus_in_gag(Amount, s(C)))
U10_gga(Amount, Coins, plus_out_gag(s(X5))) → U11_gga(ways_in_gga(Amount, Coins))
U11_gga(ways_out_gga(N)) → ways_out_gga(N)
U6_gga(C, Coins, NewAmount, ways_out_gga(N1)) → U7_gga(N1, ways_in_gga(NewAmount, .(s(C), Coins)))
U7_gga(N1, ways_out_gga(N2)) → U8_gga(plus_in_gga(N1, N2))
plus_in_gga(0, X) → U2_gga(X, nat_in_g(X))
U2_gga(X, nat_out_g) → plus_out_gga(X)
plus_in_gga(s(X), Y) → U3_gga(plus_in_gga(X, Y))
U3_gga(plus_out_gga(Z)) → plus_out_gga(s(Z))
U8_gga(plus_out_gga(N)) → ways_out_gga(N)
ways_in_gga(x0, x1)
=_in_ga(x0)
U4_gga(x0, x1, x2, x3)
plus_in_gag(x0, x1)
nat_in_g(x0)
U1_g(x0)
U2_gag(x0, x1)
U3_gag(x0)
U5_gga(x0, x1, x2, x3)
U9_gga(x0, x1, x2, x3)
U10_gga(x0, x1, x2)
U11_gga(x0)
U6_gga(x0, x1, x2, x3)
U7_gga(x0, x1)
plus_in_gga(x0, x1)
U2_gga(x0, x1)
U3_gga(x0)
U8_gga(x0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
U4_GGA(s(x3), z1, z2, =_out_ga(s(x3))) → U5_GGA(s(x3), z1, z2, U3_gag(plus_in_gag(z1, x3)))
POL(.(x1, x2)) = 0
POL(0) = 0
POL(=_in_ga(x1)) = 0
POL(=_out_ga(x1)) = 0
POL(U10_gga(x1, x2, x3)) = 0
POL(U11_gga(x1)) = 0
POL(U1_g(x1)) = 0
POL(U2_gag(x1, x2)) = x1
POL(U2_gga(x1, x2)) = 0
POL(U3_gag(x1)) = x1
POL(U3_gga(x1)) = 0
POL(U4_GGA(x1, x2, x3, x4)) = x1
POL(U4_gga(x1, x2, x3, x4)) = 0
POL(U5_GGA(x1, x2, x3, x4)) = x4
POL(U5_gga(x1, x2, x3, x4)) = 0
POL(U6_GGA(x1, x2, x3, x4)) = x3
POL(U6_gga(x1, x2, x3, x4)) = 0
POL(U7_gga(x1, x2)) = 0
POL(U8_gga(x1)) = 0
POL(U9_gga(x1, x2, x3, x4)) = 0
POL(WAYS_IN_GGA(x1, x2)) = x1
POL([]) = 0
POL(nat_in_g(x1)) = 0
POL(nat_out_g) = 0
POL(plus_in_gag(x1, x2)) = x2
POL(plus_in_gga(x1, x2)) = 0
POL(plus_out_gag(x1)) = x1
POL(plus_out_gga(x1)) = 0
POL(s(x1)) = 1 + x1
POL(ways_in_gga(x1, x2)) = 0
POL(ways_out_gga(x1)) = 0
plus_in_gag(0, X) → U2_gag(X, nat_in_g(X))
plus_in_gag(s(X), s(Z)) → U3_gag(plus_in_gag(X, Z))
U3_gag(plus_out_gag(Y)) → plus_out_gag(Y)
U2_gag(X, nat_out_g) → plus_out_gag(X)
U6_GGA(C, Coins, NewAmount, ways_out_gga(N1)) → WAYS_IN_GGA(NewAmount, .(s(C), Coins))
WAYS_IN_GGA(Amount, .(s(C), Coins)) → U4_GGA(Amount, C, Coins, =_out_ga(Amount))
U5_GGA(Amount, C, Coins, plus_out_gag(NewAmount)) → U6_GGA(C, Coins, NewAmount, ways_in_gga(Amount, Coins))
ways_in_gga(0, X1) → ways_out_gga(s(0))
ways_in_gga(X2, []) → ways_out_gga(0)
ways_in_gga(Amount, .(s(C), Coins)) → U4_gga(Amount, C, Coins, =_in_ga(Amount))
=_in_ga(X) → =_out_ga(X)
U4_gga(Amount, C, Coins, =_out_ga(s(X3))) → U5_gga(Amount, C, Coins, plus_in_gag(s(C), Amount))
plus_in_gag(0, X) → U2_gag(X, nat_in_g(X))
nat_in_g(0) → nat_out_g
nat_in_g(s(X)) → U1_g(nat_in_g(X))
U1_g(nat_out_g) → nat_out_g
U2_gag(X, nat_out_g) → plus_out_gag(X)
plus_in_gag(s(X), s(Z)) → U3_gag(plus_in_gag(X, Z))
U3_gag(plus_out_gag(Y)) → plus_out_gag(Y)
U5_gga(Amount, C, Coins, plus_out_gag(NewAmount)) → U6_gga(C, Coins, NewAmount, ways_in_gga(Amount, Coins))
ways_in_gga(Amount, .(s(C), Coins)) → U9_gga(Amount, C, Coins, =_in_ga(Amount))
U9_gga(Amount, C, Coins, =_out_ga(s(X4))) → U10_gga(Amount, Coins, plus_in_gag(Amount, s(C)))
U10_gga(Amount, Coins, plus_out_gag(s(X5))) → U11_gga(ways_in_gga(Amount, Coins))
U11_gga(ways_out_gga(N)) → ways_out_gga(N)
U6_gga(C, Coins, NewAmount, ways_out_gga(N1)) → U7_gga(N1, ways_in_gga(NewAmount, .(s(C), Coins)))
U7_gga(N1, ways_out_gga(N2)) → U8_gga(plus_in_gga(N1, N2))
plus_in_gga(0, X) → U2_gga(X, nat_in_g(X))
U2_gga(X, nat_out_g) → plus_out_gga(X)
plus_in_gga(s(X), Y) → U3_gga(plus_in_gga(X, Y))
U3_gga(plus_out_gga(Z)) → plus_out_gga(s(Z))
U8_gga(plus_out_gga(N)) → ways_out_gga(N)
ways_in_gga(x0, x1)
=_in_ga(x0)
U4_gga(x0, x1, x2, x3)
plus_in_gag(x0, x1)
nat_in_g(x0)
U1_g(x0)
U2_gag(x0, x1)
U3_gag(x0)
U5_gga(x0, x1, x2, x3)
U9_gga(x0, x1, x2, x3)
U10_gga(x0, x1, x2)
U11_gga(x0)
U6_gga(x0, x1, x2, x3)
U7_gga(x0, x1)
plus_in_gga(x0, x1)
U2_gga(x0, x1)
U3_gga(x0)
U8_gga(x0)